Skip to content

refactor: split lake docs into focused modules - #950

Closed
tydeu wants to merge 3 commits into
nightly-testingfrom
lake-split
Closed

tydeu wants to merge 3 commits into
nightly-testingfrom
lake-split

Conversation

@tydeu

@tydeu tydeu commented Sep 24, 2026 •

Copy link
Copy Markdown
Member

Splits the main Lake module into smaller modules focused on distinct subsections. It is also promotes a number of subsections into top-level sections instead of subsections of "Concepts and Terminology":

  • "Builds" and "Facets" have become a top-level "Builds" section with "Facets" as a subsection.
  • "GitHub Release Builds", "Artifact Caches", and "Remote Artifact Caches" were made subsections of a single top-level section on "Caching Builds" placed immediately after "Builds".
  • "Scripts" and "Test and Lint Drivers" have become subsections of a top-level section on "Development Workflows".

"Caching Builds" and "Development Workflows" both start with a new preface introducing their overall shared goal (facilitating development workflows and reusing build artifacts, respectively).

The main Lake module's introduction has been updated to account for the new structure and each element in the responsibility now includes a link for its key term (builds, dependencies, Reservoir, and development workflows).

@leanprover-bot leanprover-bot added the HTML available HTML has been generated for this PR label Sep 24, 2026
@tydeu
tydeu marked this pull request as ready for review September 24, 2026 06:00
@github-actions

Copy link
Copy Markdown
Contributor

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 53d6304.

@tydeu

tydeu commented Sep 25, 2026

Copy link
Copy Markdown
Member Author

Closed in favor of #952 (branched off main).

@tydeu tydeu closed this Sep 25, 2026
@tydeu
tydeu deleted the lake-split branch September 25, 2026 21:34
@tydeu
tydeu restored the lake-split branch September 25, 2026 21:34
@tydeu
tydeu deleted the lake-split branch September 28, 2026 14:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

HTML available HTML has been generated for this PR

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants